g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
P(s(x), x) → GT(x, x)
P(s(x), s(y)) → GT(x, y)
GT(s(x), s(y)) → GT(x, y)
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
N(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
F(s(x)) → H(x)
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
P(s(x), s(y)) → ID(x)
MINUS(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
P(s(x), s(y)) → IF(gt(x, y), x, y)
NOT(x) → IF(x, false, true)
P(s(x), s(y)) → NOT(gt(x, y))
G(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → N(s(x), s(y))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
M(s(x), s(y)) → M(x, y)
H(s(x)) → F(x)
K(s(x), s(y)) → K(minus(x, y), s(y))
P(s(x), x) → ID(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → F(s(y))
G(s(x), s(y)) → F(s(x))
K(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
P(s(x), x) → GT(x, x)
P(s(x), s(y)) → GT(x, y)
GT(s(x), s(y)) → GT(x, y)
G(s(x), s(y)) → M(x, y)
P(s(x), s(y)) → IF(not(gt(x, y)), id(x), id(y))
N(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → AND(f(s(x)), f(s(y)))
F(s(x)) → H(x)
P(id(x), s(y)) → GT(s(y), y)
G(s(x), s(y)) → K(minus(m(x, y), n(x, y)), s(s(0)))
P(s(x), s(y)) → ID(x)
MINUS(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
P(s(x), s(y)) → IF(gt(x, y), x, y)
NOT(x) → IF(x, false, true)
P(s(x), s(y)) → NOT(gt(x, y))
G(s(x), s(y)) → N(x, y)
G(s(x), s(y)) → T(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0)))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
G(s(x), s(y)) → N(s(x), s(y))
G(s(x), s(y)) → K(n(s(x), s(y)), s(s(0)))
M(s(x), s(y)) → M(x, y)
H(s(x)) → F(x)
K(s(x), s(y)) → K(minus(x, y), s(y))
P(s(x), x) → ID(x)
P(s(x), x) → IF(gt(x, x), id(x), id(x))
G(s(x), s(y)) → IF(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
G(s(x), s(y)) → F(s(y))
G(s(x), s(y)) → F(s(x))
K(s(x), s(y)) → MINUS(x, y)
G(s(x), s(y)) → MINUS(m(x, y), n(x, y))
P(id(x), s(y)) → IF(gt(s(y), y), y, s(y))
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), s(y)) → ID(y)
T(x) → P(x, x)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(x), s(y)) → GT(x, y)
The value of delta used in the strict ordering is 1.
POL(s(x1)) = 1 + x_1
POL(GT(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
F(s(x)) → H(x)
H(s(x)) → F(x)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(s(x)) → H(x)
H(s(x)) → F(x)
The value of delta used in the strict ordering is 8.
POL(H(x1)) = (4)x_1
POL(s(x1)) = 4 + (4)x_1
POL(F(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
MINUS(s(x), s(y)) → MINUS(x, y)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINUS(s(x), s(y)) → MINUS(x, y)
The value of delta used in the strict ordering is 1.
POL(MINUS(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
P(s(x), s(y)) → P(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))
P(id(x), s(y)) → P(x, if(gt(s(y), y), y, s(y)))
P(s(x), x) → P(if(gt(x, x), id(x), id(x)), s(x))
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
K(s(x), s(y)) → K(minus(x, y), s(y))
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
K(s(x), s(y)) → K(minus(x, y), s(y))
The value of delta used in the strict ordering is 1/16.
POL(K(x1, x2)) = (1/4)x_1
POL(minus(x1, x2)) = 1/4 + x_1
POL(s(x1)) = 1/2 + (4)x_1
POL(0) = 0
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
M(s(x), s(y)) → M(x, y)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
M(s(x), s(y)) → M(x, y)
The value of delta used in the strict ordering is 1.
POL(s(x1)) = 1 + x_1
POL(M(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
N(s(x), s(y)) → N(x, y)
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
N(s(x), s(y)) → N(x, y)
The value of delta used in the strict ordering is 1.
POL(N(x1, x2)) = x_2
POL(s(x1)) = 1 + x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
G(s(x), s(y)) → G(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))
G(s(x), s(y)) → G(minus(m(x, y), n(x, y)), n(s(x), s(y)))
g(s(x), s(y)) → if(and(f(s(x)), f(s(y))), t(g(k(minus(m(x, y), n(x, y)), s(s(0))), k(n(s(x), s(y)), s(s(0))))), g(minus(m(x, y), n(x, y)), n(s(x), s(y))))
n(0, y) → 0
n(x, 0) → 0
n(s(x), s(y)) → s(n(x, y))
m(0, y) → y
m(x, 0) → x
m(s(x), s(y)) → s(m(x, y))
k(0, s(y)) → 0
k(s(x), s(y)) → s(k(minus(x, y), s(y)))
t(x) → p(x, x)
p(s(x), s(y)) → s(s(p(if(gt(x, y), x, y), if(not(gt(x, y)), id(x), id(y)))))
p(s(x), x) → p(if(gt(x, x), id(x), id(x)), s(x))
p(0, y) → y
p(id(x), s(y)) → s(p(x, if(gt(s(y), y), y, s(y))))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
id(x) → x
if(true, x, y) → x
if(false, x, y) → y
not(x) → if(x, false, true)
and(x, false) → false
and(true, true) → true
f(0) → true
f(s(x)) → h(x)
h(0) → false
h(s(x)) → f(x)
gt(s(x), 0) → true
gt(0, y) → false
gt(s(x), s(y)) → gt(x, y)